$\forall$$A$, $B$:Type, $a$:EqDecider($A$), $b$:EqDecider($B$).
\\[0ex]sum{-}deq($A$;$B$;$a$;$b$) $\in$ ($\forall$$p$, $q$:$A$+$B$. $p$ $=$ $q$ $\Leftrightarrow$ sumdeq($a$;$b$)($p$,$q$))